es:ES, e':E, P:({e:E| loc(e) = loc(e')  Id }Prop). (e<e'. P(e))  Prop 

latex

Definitions	e<e'. P(e), x(s), Prop, E, ES, Id, loc(e), (e <loc e'), P & Q, x:A. B(x), t  T, A, False, P  Q, b
Lemmas	es-loc-pred, es-loc wf, Id wf, event system wf, es-E wf, es-locl wf